Nuprl Lemma : inr_wf
4,23
postcript
pdf
x
:Top. inr(
x
)
Decision
latex
Definitions
Decision
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
origin
x:Top. inr(x) 
Decision x:Top. inr(x) Decision x:A. B(x) T